Nuprl Definition : ma-declm
11,40
postcript
pdf
rcv(
l
,
tg
) declared in
M
==
rcv(
l
,
tg
)
dom((
M
.2).1)
latex
clarification:
rcv(
l
,
tg
) declared in
M
==
fpf-dom(KindDeq; rcv(
l
,
tg
); ((
M
.2).1))
latex
Definitions
b
,
x
dom(
f
)
,
KindDeq
,
rcv(
l
,
tg
)
,
t
.1
,
t
.2
FDL editor aliases
ma-declm
origin
rcv(l,tg) 
dom((M.2).1)
fpf-dom(KindDeq; rcv(l,tg); ((M.2).1)) rcv(l,tg) dom((M.2).1)
fpf-dom(KindDeq; rcv(l,tg); ((M.2).1)) b dom(f)